Inference at * 2 0 1 2 2 0 
Iof proof for Lemma multiply nat wf:

.....wf..... NILNIL

1. 
  (0  0 )   

latex

 by PERMUTE{1:n, 1:n} 

latex

 1: .....subterm..... T:t1:n

 1:   0  
 .

Definitions	f(a), x:AB(x), , s = t, #$n, i  j , , , x:A. B(x), t  T
Lemmas	ge wf